Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Exclusive capabilities #22218

Draft
wants to merge 32 commits into
base: main
Choose a base branch
from
Draft

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Dec 16, 2024

A draft PR to implement Capybara-like mutation checking

@Linyxus
Copy link
Contributor

Linyxus commented Dec 16, 2024

scapybara

@odersky odersky force-pushed the exclusive-capabilities branch 2 times, most recently from 8cbc022 to 0a73a26 Compare December 21, 2024 14:01
@odersky
Copy link
Contributor Author

odersky commented Dec 21, 2024

The earliest European representation of a capybara from "A Relation of a voyage" (1698)

image

When printing a type `C^` where `C` extends `Capability`, don't show the `^`.
This is overridden under -Yprint-debug.
Add dedicated tests `isMutableVar` and `isMutableVarOrAccessor`
where we now check for the `Mutable` flag. This will allow to use
`Mutable` also for update methods, so that we don't have to burn
another flag bit for them.
Also, add design document from papers to docs/internals
This means Mutable classes get {cap.rd} as default capture set.
….toCap

If existentials are mapped to fresh, it matters where they are opened. Pure or not
arguments don't have anything to do with that.
Don't add elements to hidden sets if they were subsumed previously.
 - Always store new types on rechecking
 - Store them in a hashmap which is associated with the rechecker of the
   current compilation unit
 - After rechecking is done, the map is forgotten, unless keepTypes is true.
   Under keepTypes, then map is kept in an attachment of the unit's root tree.

Change in nomenclature:

    knownType --> nuType
    rememberType --> setNuType
    hasRememberedType --> hasNuType
 - Use unsafeAssumeSeparate(...) as an escape hatch
 - In ++, use a FrozenSepState in order not to pollute hidden sets
 - This avoids two spurious separation failures in stdlib
The subsumes check mistakenly allowed any capability to subsume `cap`, since `cap` is expanded
as `caps.cap`, and by the path subcapturing rule `caps.cap <: caps`, where the capture set of
`caps` is empty. This allowed quite a few hidden errors to go through. This commit fixes the
subcapturing issue and all downstream issues caused by that fix.

In particular:

 - Don't use path comparison for `x subsumes caps.cap`

 - Don't allow an opened existential on the left of a comparison to leak into a capture set on
   the right. This would give a "leak" error later in healCaptures.

 - Print `Fresh.Cap` as `fresh` in error messages where both `cap` and `Fresh.Cap` are printed.
   This avoid confustion with `cap`. Similarly, print `A => B` as `A ->{fresh B` in that case.

 - Print pre-cc annotated capturing types with @retains annotations with `^`. The annotation is
   already rendered as a set in this case, but the `^` was missing.

 - Don't recheck `_` right hand sides of uninitialized variables. These were handled in ways
   that broke freshness checking. The new `uninitialied` scheme does not have this problem.

 - Convert cap to fresh in type arguments of asInstanceOf

 - Have Fresh.FromCap also work for pre-cc @retains annotated types

 - Don't cache captureSetOfInfos under mode IgnoreCaptures

 - Let cap and Fresh.Cap subsume other refs only if these others refs cannot
   be added separately to a capture set.

 - When creating a instance of a capability class, assume fresh.cap, not cap as capability.

Three tests had to be disabled, they were renamed from test.scala to test.scala.disabled.
Two of these will work again when we stop boxing alias types (next commit). The third,
ex-fun-aliases needs more investigation. Also, the neg test box-adapt-cases needs
to be re-evaluated.
This is necessary because the compiler is free in previous phases to dealias or not.
Therefore, capture checking should not depend on aliasing. The main difference is that
now arguments to type aliases are not necessarily boxed. They are boxed only if they need
boxing in the dealiased type.
@odersky odersky force-pushed the exclusive-capabilities branch from 0da66e2 to eae9c07 Compare December 31, 2024 17:29
The previous meaning did not do enough in the presence of fresh.
The new meaning is that all universal capture sets under a @uncheckedCaptures
become <fluid> capture sets.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants